(* Time-stamp: <modified the 09/06/2023 (at 16:18) by Erwan Jahier> *)


(** Generate smv programs

- simple equations and (memoryless) function calls are put in the ASSIGN section
- asserts are put in the INVAR section
- node calls (with memory) are put in the TRANS section
- if the first boolean output is named ok, the SPEC section contains
  AG ok
*)

let (string_of_soc_key : Soc.key -> string) = Soc2cIdent.get_soc_name


(* XXX add a CLi argument ? *)
let integer = "0..100"


let rec (type_to_string_gen : bool -> Data.t -> string) =
  fun alias v ->
    let str =
      match v with
        | String -> "string"
        | Bool -> "boolean"
        | Int  -> integer
        | Real -> "real"
        | Extern _s -> "string" (* what else should be done? *)
        (*  | Enum  (s, sl) -> "enum " ^ s ^ " {" ^ (String.concat ", " sl) ^ "}" *)
        | Enum  (s, _sl) -> s
        | Struct (sid,_) -> sid
        | Array (ty, sz) -> Printf.sprintf "%s^%d" (type_to_string_gen alias ty) sz
        | Alpha nb ->
        (* On génère des "types" à la Caml : 'a, 'b, 'c, etc. *)
          let a_value = Char.code('a') in
          let z_value = Char.code('z') in
          let str =
            if (nb >= 0 && nb <= (z_value - a_value)) then
              ("'" ^ (Char.escaped (Char.chr(a_value + nb))))
            else
              ("'a" ^ (string_of_int nb))
          in
          str

        | Alias(n,t) -> if alias then n else type_to_string_gen alias t
    in
    str

let (type_to_string : Lic.type_ -> string) = function
  | Bool_type_eff -> "boolean"
  | Int_type_eff  -> integer
  | Real_type_eff -> assert false
  | External_type_eff (_name) -> assert false
  | Abstract_type_eff (_name, _t) -> assert false
  | Enum_type_eff (name, _) -> Lv6Id.no_pack_string_of_long name
  | Array_type_eff (_ty, _sz) -> assert false
  | Struct_type_eff (_name, _) -> assert false
  | TypeVar _ -> assert false


let (type_to_string_alias : Data.t -> string) = type_to_string_gen true

open Printf
open Lic

let (f: Lv6MainArgs.t -> LicPrg.t -> Lv6Id.idref option -> unit) =
  fun opt licprg main_node ->

  let main_node_exp = LicPrg.get_main_node_exp licprg main_node in

  let _base0 = if opt.outfile <> "" then opt.outfile else
      let file = List.hd opt.infiles in
      try (Filename.chop_extension (Filename.basename file))
      with _ ->
	print_string ("*** Error: '"^file^"'is a bad file name.\n"); exit 2
  in
  let base0 = Filename.chop_extension (Filename.basename (
      Lxm.file  main_node_exp.lxm))
  in
  let dir = Lv6MainArgs.global_opt.Lv6MainArgs.dir in
  let base = Filename.concat dir base0 in
  let smv_file = base ^ ".smv" in
  let oc = open_out smv_file in


  let inputs = main_node_exp.inlist_eff in
  let outputs = main_node_exp.outlist_eff in
  let locals = match main_node_exp.loclist_eff with Some l-> l | None -> [] in
  let p = Printf.fprintf oc "%s" in
  let pn = Printf.fprintf oc "%s\n" in

  Lv6util.entete oc "--" "" ;
  pn "MODULE main
VAR";
  p "";
  let decl_var v = Printf.fprintf oc "  %s: %s;\n" v.var_name_eff (type_to_string v.var_type_eff) in
  List.iter decl_var inputs;
  List.iter decl_var outputs;
  List.iter decl_var locals;

  pn "INVAR";

  pn "ASSIGN";

  pn (sprintf "SPEC AG %s;" (List.hd outputs).var_name_eff);

  pn "TRANS";

  close_out oc;
  Printf.eprintf "W: %s has been generated.\n%!" smv_file
